Conflict generalisation #242

rtaupe · 2020-03-23T11:16:18Z

Related issue: #115

codecov · 2020-03-23T11:42:12Z

Codecov Report

Merging #242 into master will decrease coverage by 0.12%.
The diff coverage is 74.79%.

@@             Coverage Diff              @@
##             master     #242      +/-   ##
============================================
- Coverage     76.83%   76.71%   -0.13%     
- Complexity     2056     2065       +9     
============================================
  Files           150      153       +3     
  Lines          6782     6866      +84     
  Branches       1184     1188       +4     
============================================
+ Hits           5211     5267      +56     
- Misses         1177     1202      +25     
- Partials        394      397       +3

Impacted Files	Coverage Δ	Complexity Δ
...n/java/at/ac/tuwien/kr/alpha/common/AtomStore.java	`100.00% <ø> (ø)`	`6.00 <0.00> (ø)`
.../java/at/ac/tuwien/kr/alpha/solver/Antecedent.java	`0.00% <0.00%> (ø)`	`0.00 <0.00> (?)`
...va/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java	`60.42% <0.00%> (ø)`	`57.00 <0.00> (ø)`
...n/kr/alpha/solver/SolverMaintainingStatistics.java	`37.50% <ø> (ø)`	`1.00 <0.00> (ø)`
.../alpha/grounder/atoms/BodyRepresentingLiteral.java	`42.85% <42.85%> (ø)`	`2.00 <2.00> (?)`
...va/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java	`67.08% <50.00%> (-0.45%)`	`31.00 <0.00> (ø)`
.../at/ac/tuwien/kr/alpha/common/NonGroundNoGood.java	`53.48% <53.48%> (ø)`	`10.00 <10.00> (?)`
...main/java/at/ac/tuwien/kr/alpha/common/NoGood.java	`71.87% <57.14%> (-0.66%)`	`47.00 <2.00> (+1.00)`	⬇️
...t/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java	`97.91% <98.18%> (-0.42%)`	`23.00 <21.00> (ø)`
.../at/ac/tuwien/kr/alpha/common/NoGoodInterface.java	`100.00% <100.00%> (ø)`	`5.00 <1.00> (+1.00)`
... and 13 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 2239eb3...aa79539. Read the comment docs.

if atom not implied by conflict reason

that generalises conflicts

# Conflicts: # src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java

(for upcoming conflict generalisation)

(before, we went to far in some cases and did too many resolutions when computing the 1UIP)

(esp. try in other direction if first direction fails)

because tested classes are also in common package

(i.e., does not start with _ or upper-case letter) (this is mainly to notice errors in unit tests!)

…sation

... none learned from nogood violated most often

if further resolution is not possible

that made nogoods too small by mapping different variables to the same new variable name

(to learn better nogoods in the case of 3col_crafted)

rtaupe added 7 commits March 20, 2020 13:19

Add references to original nogoods to Antecedents

5e41ba8

Introduce NonGroundNoGood

a5c6a9b

Generate first non-ground nogood (for head of rule)

0cf2dbc

Generate non-ground nogoods for static rule nogoods

16ca3fe

Reset rule IDs before running tests

2d8689d

Satisfy Checkstyle

ff97640

Generate non-ground nogoods for static constraint nogoods

46b9883

rtaupe added 22 commits March 23, 2020 15:24

Remember original nogoods in binary watch list

b545c27

Learn non-ground nogoods (preliminary implementation)

95e5914

Include variables in non-ground rule atom

350e7ab

Fix: do not try to find atom in conflict reason

674aa8f

if atom not implied by conflict reason

Do not add the same original nogood twice to binary watch list

e628068

Remove faulty code from conflict generalisation

e84056f

Skeleton for separate conflict analysis method

2f20021

that generalises conflicts

Remove conflict generalisation code from #analyzeTrailBased

d7c1b25

Merge branch 'master' into conflict_generalisation

21de49b

# Conflicts: # src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java

Extract ConflictAnalysisResult to separate file

ecd6bd4

Re-implement CDNL without 1UIP

d19f95a

(for upcoming conflict generalisation)

Learn nogoods on all UIPs

5c628ea

Use underlying ground learner in non-ground learner

bc1957e

Fix re-implementation of 1UIP learning by using trail walker

a37eceb

(before, we went to far in some cases and did too many resolutions when computing the 1UIP)

If current DL = 0, learn nothing and return UNSAT

af1160e

1UIP learning: consider sophisticated techniques to prove UNSAT

0cb9bcc

Make variable names unique in nogoods before resolution

0cfa69c

Move substitution stuff from grounder to common

e838da0

Fix visibility of Substitution constructor and method

4de090c

Implement explanation-based learning of non-ground constraints

5c24ad9

Substitution: left constant / right variable is unsupported

498a008

Fix get...Variables in BodyRepresentingLiteral

19d1fec

rtaupe added 5 commits April 7, 2020 17:35

Fix unification of conflicting atoms during non-ground resolution

dc663bc

Satisfy Checkstyle

ae2cfc3

Apply conflict unifier to whole non-ground nogood

2c33c21

Implement NonGroundNoGood#equals() and hashCode() and compareTo

b4cdc6b

Enable more kinds of unifiers

b27e283

(esp. try in other direction if first direction fails)

rtaupe marked this pull request as draft April 10, 2020 07:12

rtaupe changed the title ~~WIP: Conflict generalisation~~ Conflict generalisation Apr 10, 2020

rtaupe added 23 commits April 17, 2020 17:05

stop conflict generalisation after 1000 conflicts

edc03ca

Move SubsitutionTest to common package

1a5660f

because tested classes are also in common package

Move SubsitutionTest to common package

b3484a0

because tested classes are also in common package

Merge branch 'move_substitution_test' into conflict_generalisation

87adc46

move method parseTerm from Substitution to ProgramPartParser

fafecf1

use ProgramPartParser to construct literals for unit tests

80b0cf1

Merge branch 'program_part_parser' into conflict_generalisation

06d8199

Fix: ProgramPartParser must accept variables

d61a4a6

Merge branch 'program_part_parser' into conflict_generalisation

7ae49ea

Throw exception if variable name is invalid

9c47b90

(i.e., does not start with _ or upper-case letter) (this is mainly to notice errors in unit tests!)

Merge branch 'forbid_lowercase_variable_terms' into conflict_generali…

18c50ba

…sation

Do not learn multiple equivalent non-ground nogoods

6934d80

Output most effective learned non-ground nogoods as constraints

a877134

Simplify variable names in learned nogoods

2e89d91

Further simplify variable names in learned nogoods

276b8d5

Do not attempt to print violated nogoods if there are none

fa045d0

Satisfy CheckStyle

ef7a796

Log all learned non-ground nogoods if ...

d84305a

... none learned from nogood violated most often

Learn non-ground nogood from non-UIP

5a5f6a2

if further resolution is not possible

Output all learned constraints ordered by number of violations

cf8a47f

Fix bug in NonGroundNoGood#simplifyVariableNames

d56eea4

that made nogoods too small by mapping different variables to the same new variable name

use also literals assigned at DL below current DL for resolution

f5e8824

(to learn better nogoods in the case of 3col_crafted)

Satisfy CheckStyle

aa79539

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Conflict generalisation #242

Conflict generalisation #242

rtaupe commented Mar 23, 2020

codecov bot commented Mar 23, 2020 •

edited

Loading

Conflict generalisation #242

Are you sure you want to change the base?

Conflict generalisation #242

Conversation

rtaupe commented Mar 23, 2020

codecov bot commented Mar 23, 2020 • edited Loading

Codecov Report

codecov bot commented Mar 23, 2020 •

edited

Loading